es:ES, i:Id, ds:x:Id fp Type, da:k:Knd fp Type. es-decls(es;i;ds;da)  Prop 

latex

Definitions	Id, Knd, es-decls(es;i;ds;da), xL.P(x), ES, (x  l), fpf-domain(f), vartype(i;x), let x = a in b(x), f(x), E, P  Q, loc(e), isrcv(e), Prop, kind(e), valtype(e), b, IdDeq, P  Q, P & Q, P  Q, P  Q, a:A fp B(a), Top, x. t(x), x:A. B(x), KindDeq, t  T
Lemmas	Kind-deq wf, Knd wf, fpf-trivial-subtype-top, member-fpf-domain, id-deq wf, Id wf, es-valtype wf, subtype rel wf, es-kind wf, es-isrcv wf, assert wf, es-loc wf, es-E wf, fpf-ap wf, let wf, es-vartype wf, fpf-domain wf, l member wf, l-all wf, event system wf, fpf wf